nLab mere proposition

Mere Propositions

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Mere Propositions

Idea

In homotopy type theory, the notion of mere proposition is an internalization of the notion of proposition / (-1)-truncated object. Mere propositions are also called h-propositions, types of h-level 11, (1)(-1)-truncated types, or even just propositions if no ambiguity will result. Semantically, mere propositions correspond to (-1)-groupoids or more generally (-1)-truncated objects.

Mere propositions are one way to embed logic into homotopy type theory, via the propositions as some types / bracket types approach. For many purposes, this is the “correct” way to embed logic (as opposed to the propositions as types approach — for instance, the PAT version of excluded middle contradicts the univalence axiom, whereas the mere-propositional version does not).

Definition

Consider intensional type theory with dependent sums, dependent products, and identity types.

There are many equivalent definitions of a type being an h-proposition. Perhaps the simplest is as follows.

Definition

For AA a type, let isProp(A)isProp(A) denote the dependent product of the identity types for all pairs of terms of AA:

isProp(A) x:A y:A(x=y) isProp(A) \coloneqq \prod_{x\colon A} \prod_{y\colon A} (x=y)

We say that AA is an h-proposition if isProp(A)isProp(A) is an inhabited type.

In propositions as types language, this can be pronounced as “every two elements of AA are equal”.

Proposition

The following are provably equivalent definitions of isProp(A)isProp(A):

  • isProp(A) x:A y:AisContr(x=y)isProp(A) \coloneqq \prod_{x\colon A} \prod_{y\colon A} isContr(x=y)
  • isProp(A)(AisContr(A)) isProp(A) \coloneqq (A \to isContr(A))
  • isProp(A)isEquiv(const 𝟚,A)isProp(A) \coloneqq \mathrm{isEquiv}(\mathrm{const}_{\mathbb{2}, A})
  • isProp(A) f:𝟚Af(0)=f(1)isProp(A) \coloneqq \prod_{f:\mathbb{2} \to A} f(0) = f(1)
  • isProp(A) f:𝟚AisContr(f(0)=f(1))isProp(A) \coloneqq \prod_{f:\mathbb{2} \to A} isContr(f(0) = f(1))
  • isProp(A) f:𝟚A x:𝟚 y:𝟚f(x)=f(y)isProp(A) \coloneqq \prod_{f:\mathbb{2} \to A} \prod_{x:\mathbb{2}} \prod_{y:\mathbb{2}} f(x) = f(y)
  • isProp(A) f:𝟚A p:𝕀A x:𝟚p(rec 𝟚 𝕀(0 𝕀,1 𝕀)(x))=f(x)isProp(A) \coloneqq \prod_{f:\mathbb{2} \to A} \sum_{p:\mathbb{I} \to A} \prod_{x:\mathbb{2}} p(\mathrm{rec}_\mathbb{2}^\mathbb{I}(0_\mathbb{I}, 1_\mathbb{I})(x)) = f(x)

The first fits into the general inductive definition of n-groupoid: an \infty-groupoid is an nn-groupoid if all its hom-groupoids are (n1)(n-1)-groupoids.

The second says that being a proposition is equivalent to being “contractible if inhabited”, and when isContr is expanded out to x:A y:Ax= Ay\sum_{x:A} \prod_{y:A} x =_A y, the resulting type A x:A y:Ax= AyA \to \sum_{x:A} \prod_{y:A} x =_A y is just the type of the graphs of dependent functions of x:A y:Ax= Ay\prod_{x:A} \prod_{y:A} x =_A y.

The third states that being a proposition is the same as being a bool\mathrm{bool}-local type: the function

const 𝟚,Aλx:A.λb:v.x:A(boolA)\mathrm{const}_{\mathbb{2}, A} \equiv \lambda x:A.\lambda b:v.x:A \to (\mathrm{bool} \to A)

which takes elements x:Ax:A to constant functions from the boolean domain with value xx is an equivalence of types.

The fourth states that being a proposition is equivalent to the condition that for every function from the boolean domain, f(0)=f(1)f(0) = f(1), and is interderivable from the usual definition of isProp via the recursion principle of the boolean domain.

The fifth states that being a proposition is equivalent to the condition that for every function from the boolean domain, f(0)=f(1)f(0) = f(1) is contractible, and is interderivable from the first via the recursion principle of the boolean domain.

The sixth states that being a proposition is equivalent to the condition that every function from the boolean domain is a weakly constant function, and can be proven to be equivalent to the fourth via double induction on the boolean domain and the properties of identity types.

The seventh states that being a proposition is equivalent to the condition that every function from the boolean domain to AA factors through the interval type via the function rec 𝟚 𝕀(0 𝕀,1 𝕀):𝟚𝕀\mathrm{rec}_\mathbb{2}^\mathbb{I}(0_\mathbb{I}, 1_\mathbb{I}):\mathbb{2} \to \mathbb{I} defined by the recursion principle of the boolean domain.

Rules for isProp

The usual definition of isProp is given by the following rules:

ΓAtypeΓisProp(A)typeΓAtypeΓisProp(A) x:A y:Ax= Aytype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{isProp}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{isProp}(A) \equiv \prod_{x:A} \prod_{y:A} x =_A y \; \mathrm{type}}

If the dependent type theory doesn’t have dependent function types, but still has identity types one could still define isProp by adding the formation, introduction, elimination, computation, and uniqueness rules for isProp:

Formation rules for isProp types:

ΓAtypeΓ,x:A,y:Ax= AytypeΓisProp(A)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}{\Gamma \vdash \mathrm{isProp}(A) \; \mathrm{type}}

Introduction rules for isProp types:

Γ,x:A,y:Ap(x,y):x= AyΓλ(x).λ(y).p(x,y):isProp(A)\frac{\Gamma, x:A, y:A \vdash p(x, y):x =_A y}{\Gamma \vdash \lambda(x).\lambda(y).p(x, y):\mathrm{isProp}(A)}

Elimination rules for isProp types:

Γp:isProp(A)Γa:AΓb:AΓp(a,b):a= Ab\frac{\Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash p(a, b):a =_A b}

Computation rules for isProp types:

Γ,x:A,y:Ap(x,y):x= AyΓa:AΓb:AΓβ isProp:(λ(x).λ(y).p(x,y))(a,b)= a= Abp(a,b)\frac{\Gamma, x:A, y:A \vdash p(x, y):x =_A y \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash \beta_\mathrm{isProp}:(\lambda(x).\lambda(y).p(x, y))(a, b) =_{a =_A b} p(a, b)}

Uniqueness rules for isProp types:

Γp:isProp(A)Γη isProp:p= isProp(A)λ(x).λ(y).p(x,y)\frac{\Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \eta_\mathrm{isProp}:p =_{\mathrm{isProp}(A)} \lambda(x).\lambda(y).p(x, y)}

Properties

  • We can prove that for any AA, the type isProp(A)isProp(A) is an h-proposition, i.e. isProp(isProp(A))isProp(isProp(A)). Thus, any two inhabitants of isProp(A)isProp(A) (witnesses that AA is an h-proposition) are “equal”.

  • Every function between h-propositions AA and BB is an embedding of types.

  • If AA and BB are h-props and there exist maps ABA\to B and BAB\to A, then AA and BB are equivalent. This follows from the fact that if AA and BB are types and there exists embeddings ABA\to B and BAB\to A, then AA and BB are equivalent.

Relation to the principles of omniscience

Suppose that AA is a mere proposition. Then AA is equivalent to the existential quantifier x:A.(λt.1)(x)=1\exists x:A.(\lambda t.1)(x) = 1, where λt.1\lambda t.1 is the constant function from AA to the booleans which takes elements of AA to the boolean 1:bool1:\mathrm{bool}. Then, one can show that various principles of omniscience are equivalent to weak versions of excluded middle, via the special case of the constant function λt.1\lambda t.1:

( A:Prop f:A2x:A.f(x)=1¬(x:A.f(x)=1))( A:PropA¬A)\left(\prod_{A:\mathrm{Prop}} \prod_{f:A \to 2} \exists x:A.f(x) = 1 \vee \neg (\exists x:A.f(x) = 1)\right) \simeq \left(\prod_{A:\mathrm{Prop}} A \vee \neg A\right)
( A:Prop f:A2¬(x:A.f(x)=1)¬¬(x:A.f(x)=1))( A:Prop¬A¬¬A)\left(\prod_{A:\mathrm{Prop}} \prod_{f:A \to 2} \neg (\exists x:A.f(x) = 1) \vee \neg \neg (\exists x:A.f(x) = 1)\right) \simeq \left(\prod_{A:\mathrm{Prop}} \neg A \vee \neg \neg A\right)
( A:Prop B:Prop f:A2 g:B2¬((x:A.f(x)=1)(x:B.g(x)=1))(¬(x:A.f(x)=1)¬(x:B.g(x)=1)))( A:Prop B:Prop¬(AB)(¬A)(¬B))\left(\prod_{A:\mathrm{Prop}} \prod_{B:\mathrm{Prop}} \prod_{f:A \to 2} \prod_{g:B \to 2} \neg ((\exists x:A.f(x) = 1) \wedge (\exists x:B.g(x) = 1)) \to (\neg (\exists x:A.f(x) = 1) \vee \neg (\exists x:B.g(x) = 1))\right) \simeq \left(\prod_{A:\mathrm{Prop}} \prod_{B:\mathrm{Prop}} \neg (A \wedge B) \to (\neg A) \vee (\neg B)\right)
( A:Prop f:A2¬¬(x:A.f(x)=1)x:A.f(x)=1)( A:Prop¬¬AA)\left(\prod_{A:\mathrm{Prop}} \prod_{f:A \to 2} \neg \neg (\exists x:A.f(x) = 1) \to \exists x:A.f(x) = 1\right) \simeq \left(\prod_{A:\mathrm{Prop}} \neg \neg A \to A\right)

Categorical semantics

We discuss the categorical semantics of h-propositions.

Let 𝒞\mathcal{C} be a locally cartesian closed category with sufficient structure to interpret all the above type theory. This means that CC has a weak factorization system with stable path objects, and that trivial cofibrations are preserved by pullback along fibrations between fibrant objects. (We ignore questions of coherence, which are not important for this discussion.)

Then for a fibrant object AA, the object isProp(A)isProp(A) defined above (with the first definition) is obtained by taking dependent product of the path-object A IA×AA^I \to A\times A along the projection A×A1A\times A\to 1. By adjunction, a global element of isProp(A)isProp(A) is therefore equivalent to a section of the path-object, which exactly means a (right) homotopy between the two projections A×AAA\times A\;\rightrightarrows\; A. The existence of such a homotopy, in turn, is equivalent to saying that any two maps XAX\;\rightrightarrows\; A are homotopic.

More generally, we may apply this locally. Suppose that ABA\to B is a fibration, which we can regard as a dependent type

x:BA(x):Type.x\colon B \vdash A(x)\colon Type.

Then we have a dependent type

x:BisProp(A(x)):Typex\colon B \vdash isProp(A(x))\colon Type

represented by a fibration isProp(A)BisProp(A)\to B. By applying the above argument in the slice category 𝒞/B\mathcal{C}/B, we see that isProp(A)BisProp(A)\to B has a section exactly when any two maps in 𝒞/B\mathcal{C}/B into ABA\to B are homotopic over BB. We can also construct the type

x:BisProp(A(x))\prod_{x\colon B} isProp(A(x))

in global context, which has a global element precisely when isProp(A)BisProp(A)\to B has a section.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

References

Last revised on September 6, 2024 at 22:27:07. See the history of this page for a list of all contributions to it.